FL added and tested #3574

briangmilnes · 2024-10-16T05:40:21Z

Two changes: 1) FL lexeme in FStarC_Parser_LexFStar.ml
2) tests/validation-time with a Test.LexemeFL.fst that checks FL

…alidation-time with a Test.LexemeFL.fst that checks __FL__

briangmilnes · 2024-10-16T06:31:38Z

Is this done even if it failed to post to slack? I think I'm confgured now.

mtzguido · 2024-10-16T23:03:25Z

ocaml/fstar-lib/FStarC_Parser_LexFStar.ml

@@ -473,6 +473,7 @@ match%sedlex lexbuf with
 | "#print-effects-graph" -> PRAGMA_PRINT_EFFECTS_GRAPH
 | "__SOURCE_FILE__" -> STRING (L.source_file lexbuf)
 | "__LINE__" -> INT (string_of_int (L.current_line lexbuf), false)
+ | "__FL__"   -> STRING ((L.source_file lexbuf) ^ "(" ^ (string_of_int (L.current_line lexbuf)) ^ ")")


__FL__ seems a bit obscure to me, should we maybe call this __FILELINE__? But I don't have a strong opinion, would be good if others chime in.

You have to reference it in every test so long is kind of cumbersome. For example:
let test_system n =
let r = FStar.Unix.system "echo HI" in
match r with
| WEXITED e -> if_test FL (e = 0) n None
| _ -> final_fail FL n None

I agree with Guido, I aslo find FL a bit obscure.
IMO, aggregating LINE and SOURCE_FILE in this formatting is quite opinionated and should probably be user-defined.

@briangmilnes why not using a tactic for that here, e.g.:

module Hello open FStar.Char open FStar.Tactics let fl (x: unit) (#[let sealed_range = range_of_term (quote x) in let range = unseal sealed_range in let result = FStar.Range.explode range in exact (quote result)] loc: string * int * int * int * int) = let file, line_start, col_start, _line_end, _col_end = loc in file ^ "(" ^ string_of_int line_start ^ ")" // This is line 14 let file_line: string = fl () let _ = assert_norm (file_line == "<input>(15)")

This is for logging and test packages. Nothing should be left to the user. In testing the ocaml wrap of unix and a few other things, I need the file/line 139 times. Terse is good here, although I eschew it in almost all situations.

A tactic that allows a function is a great alternative. The language server in emacs takes that and works but I can't get a command line to compile it. What's the change needed for compilation? It also has the advantage that the strings are not coming back from the lexer with strange UTF8.

Well, verbosity or terseness is a choice, right? I tend to prefer verbosity in such cases, but that's only my preference.

Nice! Here it won't work via the command line because of <input>: that's the file name given by the F* interactive protocol used by emacs I believe.
Running that from a file whose path is /tmp/Hello.fst, you should be able to assert_norm (file_line == "/tmp/Hello.fst(15)") (instead of the one I've put above).

The issue I have is it will not compile, not the string back from fl() or FL.

F*orge: VALIDATE _build/fstar/fst/checked/Hello.fst.checked

Error 168 at src/Hello.fst(8,8-8,8):

Syntax error

1 error was reported (see above)
That's the (# line on my test of it running in OCaml.

mtzguido · 2024-10-16T23:04:21Z

tests/Makefile

@@ -21,6 +21,7 @@ ALL_TEST_DIRS += vale
 ALL_TEST_DIRS += hacl
 ALL_TEST_DIRS += simple_hello
 ALL_TEST_DIRS += dune_hello
+ALL_TEST_DIRS += validation-time


The new single test here is not related to time at all? I think you can just drop Text.LexemeFL.fst in tests/micro-benchmarks and not add any new Makefiles.

validation-time is the name of the phase right? Nothing to do with time. I didn't put it in micro-benchmarks as it is a correctness test. For Unix I added a run-time test directory that I'm working on right now.

micro-benchmarks is a bad name really.. we use that directory for a whole bunch of unit tests. I'll rename it soon.

mtzguido · 2024-10-16T23:04:45Z

tests/validation-time/Test.LexemeFL.fst

+let _ = assert(fl <> "")
+let fl'  = string_of_list (list_of_string "Test.LexemFL.fst(11)")
+let _ = assert((strlen fl') = 20) by compute()
+let _ = assert(fl' = "Test.LexemFL.fst(11)") by compute()


Using assert_norm breaks the dependency on tactics (and is maybe more idiomatic).

Also what is this testing? Seems to be just that 1) fl is nonempty and 2) that string_of_list and list_of_string are inverses.
(Note the missing 'e' from 'Test.LexemFL.fst(11)'.)

No what the darn string_of_list (list_of_string is doing is getting rid of oddball characters that prevent line 13 from working to show that FL is working. See the comment line above.

I have a commit pushed with the assert_norm changes. Do I need another PR?

So I have Test.FLLexeme moved to the directory to be renamed later, micro-benchmarks and validaton-time deleted and out of the makefile.

And this FStar revision will compile Luke's fl(), which is two characters shorter and more obvious than FL. I have no idea that reflection would do this for me as it is not in the book.

It would obviate this entire PR.

Guido which way do you want it? Lexeme or Tactics?

…by compute()

briangmilnes · 2024-10-17T06:11:58Z

The tests/Makefile conflict is just adding validation-time as a test directory.

mtzguido · 2024-10-21T21:52:19Z

Hi Brian, could we rename the lexeme to __FILELINE__ and rebase this PR? (rebase so the addition of validation-time is gone from the history, I guess it would be two commits: adding the lexeme, and adding the test).

It needs a fix though: we should probably take the basename of the file instead of just L.source_file. This test works for me, when running F* from the root of the repo:

module Test.LexemeFL

let fl = __FL__
let _ = assert(fl = "tests/micro-benchmarks/Test.LexemeFL.fst(3)")

(so there are no funny characters) but the behavior of the module shouldn't depend on how the file was referred to.

Lucas' tactic-based fl is really cool, and could be used for many more things, but using tactics introduces many dependencies and this new lexeme seems reasonable enough.

FWIW the syntax error you got above is probably due to an old F*. Complex meta qualifiers like the one in Lucas' code used to require enclosing parentheses.

briangmilnes · 2024-10-21T23:57:35Z

Will do. I'm easy about all of this.

…

On Mon, Oct 21, 2024 at 2:52 PM Guido Martínez ***@***.***> wrote: Hi Brian, could we rename the lexeme to __FILELINE__ and rebase this PR? (rebase so the addition of validation-time is gone from the history, I guess it would be two commits: adding the lexeme, and adding the test). It needs a fix though: we should probably take the basename of the file instead of just L.source_file. This test works for me, when running F* from the root of the repo: module Test.LexemeFL let fl = __FL__let _ = assert(fl = "tests/micro-benchmarks/Test.LexemeFL.fst(3)") (so there are no funny characters) but the behavior of the module shouldn't depend on how the file was referred to. Lucas' tactic-based fl is really cool, and could be used for many more things, but using tactics introduces many dependencies and this new lexeme seems reasonable enough. FWIW the syntax error you got above is probably due to an old F*. Complex meta qualifiers like the one in Lucas' code used to require enclosing parentheses. — Reply to this email directly, view it on GitHub <#3574 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACKMDKYEASY4PSOYEV364ALZ4VZSTAVCNFSM6AAAAABQAUAKX2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIMRXHAYTANBYHA> . You are receiving this because you were mentioned.Message ID: ***@***.***>

briangmilnes · 2024-10-28T18:43:30Z

Too far behind, merge is not accepted on github due to some test failure, going to kill this fork and start again.

mtzguido · 2024-10-28T19:06:59Z

For the future you can just fix up your changes locally and then force push to the branch where you opened the PR from, and it will be updated.

Two changes: 1) __FL__ lexeme in FStarC_Parser_LexFStar.ml 2) tests/v…

9b114bd

…alidation-time with a Test.LexemeFL.fst that checks __FL__

mtzguido requested changes Oct 16, 2024

View reviewed changes

Moved to assert_norm instead of opening tactics and using assert(..) …

6bcf77a

…by compute()

Moved Test.LexemeFL to micro-benchmarks got rid of tests/validation-time

60f36d1

Merge branch 'master' into milnes-fl

5b221d0

briangmilnes closed this Oct 28, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

FL added and tested #3574

FL added and tested #3574

briangmilnes commented Oct 16, 2024

briangmilnes commented Oct 16, 2024

mtzguido Oct 16, 2024

briangmilnes Oct 17, 2024

W95Psp Oct 17, 2024

briangmilnes Oct 17, 2024

W95Psp Oct 17, 2024

briangmilnes Oct 17, 2024

mtzguido Oct 16, 2024

briangmilnes Oct 17, 2024

mtzguido Oct 17, 2024

mtzguido Oct 16, 2024

mtzguido Oct 16, 2024

briangmilnes Oct 17, 2024 •

edited

Loading

briangmilnes Oct 17, 2024

briangmilnes Oct 17, 2024

briangmilnes commented Oct 17, 2024

mtzguido commented Oct 21, 2024

briangmilnes commented Oct 21, 2024 via email

briangmilnes commented Oct 28, 2024

mtzguido commented Oct 28, 2024

__FL__ added and tested #3574

__FL__ added and tested #3574

Conversation

briangmilnes commented Oct 16, 2024

briangmilnes commented Oct 16, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

briangmilnes Oct 17, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

briangmilnes commented Oct 17, 2024

mtzguido commented Oct 21, 2024

briangmilnes commented Oct 21, 2024 via email

briangmilnes commented Oct 28, 2024

mtzguido commented Oct 28, 2024

FL added and tested #3574

FL added and tested #3574

briangmilnes Oct 17, 2024 •

edited

Loading